『The formal semantics of programming languages: an introduction』
Winskel, Glynn. The formal semantics of programming languages: an introduction. 5. printing, Cambridge, Mass., MIT Press, 2001, 361p., (Foundations of computing), ISBN978-0-262-23169-5. (pdf)
https://gyazo.com/f9613b642eea5b0c1b80710a051ad3b5
table:目次
1 Basic set theory 1 基本的な集合論
1.1 Logical notation … 1 1.1 論理記法 1
1.2 Sets … 2 1.2 集合 2
1.2.1 Sets and properties … 3 1.2.1 集合と性質 3
1.2.2 Some important sets … 3 1.2.2 いくつかの重要な集合 3
1.2.3 Constructions on sets … 4 1.2.3 集合の構成 4
1.2.4 The axiom of foundation … 6 1.2.4 基礎の公理 6
1.3 Relations and functions … 6 1.3 関係と関数 6
1.3.1 Lambda notation … 7 1.3.1 ラムダ記法 7
1.3.2 Composing relations and functions … 7 1.3.2 関係と関数の合成 7
1.3.3 Direct and inverse image of a relation … 9 1.3.3 関係の直接像と逆像 9
1.3.4 Equivalence relations … 9 1.3.4 同値関係 9
1.4 Further reading … 10 1.4 さらなる読書 10
2 Introduction to operational semantics 2 操作的意味論への導入
2.1 IMP-a simple imperative language … 11 2.1 IMP - 簡単な命令型言語 11
2.2 The evaluation of arithmetic expressions … 13 2.2 算術式の評価 13
2.3 The evaluation of boolean expressions … 17 2.3 論理式の評価 17
2.4 The execution of commands … 19 2.4 コマンドの実行 19
2.5 A simple proof … 20 2.5 簡単な証明 20
2.6 Alternative semantics … 24 2.6 別の意味論 24
2.7 Further reading … 26 2.7 さらなる読書 26
3 Some principles of induction 3 いくつかの帰納法の原理
3.1 Mathematical induction … 27 3.1 数学的帰納法 27
3.2 Structural induction … 28 3.2 構造的帰納法 28
3.3 Well-founded induction … 31 3.3 整礎帰納法 31
3.4 Induction on derivations … 35 3.4 導出に基づく帰納法 35
3.5 Definitions by induction … 39 3.5 帰納による定義 39
3.6 Further reading … 40 3.6 さらなる読書 40
4 Inductive definitions 4 帰納的定義
4.1 Rule induction … 41 4.1 規則帰納法(ルール帰納法) 41
4.2 Special rule induction … 44 4.2 特殊な帰納規則 44
4.3 Proof rules for operational semantics … 45 4.3 操作的意味論のための証明規則 45
4.3.1 Rule induction for arithmetic expressions … 45 4.3.1 算術式に対する規則帰納法 45
4.3.2 Rule induction for boolean expressions … 46 4.3.2 論理式に対する規則帰納法 46
4.3.3 Rule induction for commands … 47 4.3.3 コマンドに対する規則帰納法 47
4.4 Operators and their least fixed points … 52 4.4 演算子とその最小不動点 52
4.5 Further reading … 54 4.5 さらなる読書 54
5 The denotational semantics of IMP 5 IMPの意味論
5.1 Motivation … 55 5.1 動機 55
5.2 Denotational semantics … 56 5.2 意味論 56
5.3 Equivalence of the semantics … 61 5.3 意味論の同値性 61
5.4 Complete partial orders and continuous functions … 68 5.4 完全順序集合と連続関数 68
5.5 The Knaster-Tarski Theorem … 74 5.5 クナスター＝タルスキーの定理 74
5.6 Further reading … 75 5.6 さらなる読書 75
6 The axiomatic semantics of IMP 6 IMPの公理的意味論
6.1 The idea … 77 6.1 アイデア 77
6.2 The assertion language Assn … 80 6.2 述語言語 Assn 80
6.2.1 Free and bound variables … 81 6.2.1 自由変数と束縛変数 81
6.2.2 Substitution … 82 6.2.2 代入 82
6.3 Semantics of assertions … 84 6.3 述語の意味論 84
6.4 Proof rules for partial correctness … 89 6.4 部分正当性のための証明規則 89
6.5 Soundness … 91 6.5 完全性 91
6.6 Using the Hoare rules – an example … 93 6.6 ホーア規則の使用例 93
6.7 Further reading … 96 6.7 さらなる読書 96
7 Completeness of the Hoare rules 7 ホーア規則の完全性
7.1 Gödel's Incompleteness Theorem … 99 7.1 ゲーデルの不完全性定理 99
7.2 Weakest preconditions and expressiveness … 100 7.2 最弱事前条件と表現力 100
7.3 Proof of Gödel's Theorem … 110 7.3 ゲーデルの定理の証明 110
7.4 Verification conditions … 112 7.4 検証条件 112
7.5 Predicate transformers … 115 7.5 述語変換器 115
7.6 Further reading … 117 7.6 さらなる読書 117
8 Introduction to domain theory 8 領域理論への導入
8.1 Basic definitions … 119 8.1 基本的な定義 119
8.2 Streams – an example … 121 8.2 ストリームの例 121
8.3 Constructions on cpo's … 123 8.3 cpoの構成 123
8.3.1 Discrete cpo's … 124 8.3.1 離散cpo 124
8.3.2 Finite products … 125 8.3.2 有限積 125
8.3.3 Function space … 128 8.3.3 関数空間 128
8.3.4 Lifting … 131 8.3.4 リフティング 131
8.3.5 Sums … 133 8.3.5 和 133
8.4 A metalanguage … 135 8.4 メタ言語 135
8.5 Further reading … 139 8.5 さらなる読書 139
9 Recursion equations 9 再帰方程式
9.1 The language REC … 141 9.1 言語 REC 141
9.2 Operational semantics of call-by-value … 143 9.2 値渡しによる操作的意味論 143
9.3 Denotational semantics of call-by-value … 144 9.3 値渡しによる意味論的意味論 144
9.4 Equivalence of semantics for call-by-value … 149 9.4 値渡しにおける意味論の同値性 149
9.5 Operational semantics of call-by-name … 153 9.5 名前渡しによる操作的意味論 153
9.6 Denotational semantics of call-by-name … 154 9.6 名前渡しによる意味論的意味論 154
9.7 Equivalence of semantics for call-by-name … 157 9.7 名前渡しにおける意味論の同値性 157
9.8 Local declarations … 161 9.8 ローカルな宣言 161
9.9 Further reading … 162 9.9 さらなる読書 162
10 Techniques for recursion 10 再帰の技法
10.1 Bekič's Theorem … 165 10.1 ベキッチの定理 165
10.2 Fixed-point induction … 166 10.2 不動点帰納法 166
10.3 Well-founded induction … 174 10.3 整礎帰納法 174
10.4 Well-founded recursion … 176 10.4 整礎再帰 176
10.5 An exercise … 179 10.5 演習 179
10.6 Further reading … 181 10.6 さらなる読書 181
11 Languages with higher types 11 高階型を持つ言語
11.1 An eager language … 183 11.1 即時評価言語 183
11.2 Eager operational semantics … 186 11.2 即時評価の操作的意味論 186
11.3 Eager denotational semantics … 188 11.3 即時評価の意味論的意味論 188
11.4 Agreement of eager semantics … 190 11.4 即時評価における意味論の一致 190
11.5 A lazy language … 200 11.5 遅延評価言語 200
11.6 Lazy operational semantics … 201 11.6 遅延評価の操作的意味論 201
11.7 Lazy denotational semantics … 203 11.7 遅延評価の意味論的意味論 203
11.8 Agreement of lazy semantics … 204 11.8 遅延評価における意味論の一致 204
11.9 Fixed-point operators … 209 11.9 不動点演算子 209
11.10 Observations and full abstraction … 215 11.10 観測と完全抽象 215
11.11 Sums … 219 11.11 和型 219
11.12 Further reading … 221 11.12 さらなる読書 221
12 Information systems 12 情報システム
12.1 Recursive types … 223 12.1 再帰型 223
12.2 Information systems … 225 12.2 情報システム 225
12.3 Closed families and Scott predomains … 228 12.3 閉じた集合族とスコット予領域 228
12.4 A cpo of information systems … 233 12.4 情報システムのcpo 233
12.5 Constructions … 236 12.5 構成 236
12.5.1 Lifting … 237 12.5.1 リフティング 237
12.5.2 Sums … 239 12.5.2 和 239
12.5.3 Product … 241 12.5.3 積 241
12.5.4 Lifted function space … 243 12.5.4 リフティングされた関数空間 243
12.6 Further reading … 247 12.6 さらなる読書 247
13 Recursive types 13 再帰型
13.1 An eager language … 251 13.1 即時評価言語 251
13.2 Eager operational semantics … 255 13.2 即時評価の操作的意味論 255
13.3 Eager denotational semantics … 257 13.3 即時評価の意味論的意味論 257
13.4 Adequacy of eager semantics … 262 13.4 即時評価における意味論の適合性 262
13.5 The eager λ-calculus … 267 13.5 即時評価のλ計算 267
13.5.1 Equational theory … 269 13.5.1 等式理論 269
13.5.2 A fixed-point operator … 272 13.5.2 不動点演算子 272
13.6 A lazy language … 278 13.6 遅延評価言語 278
13.7 Lazy operational semantics … 278 13.7 遅延評価の操作的意味論 278
13.8 Lazy denotational semantics … 281 13.8 遅延評価の意味論的意味論 281
13.9 Adequacy of lazy semantics … 288 13.9 遅延評価における意味論の適合性 288
13.10 The lazy λ-calculus … 290 13.10 遅延評価のλ計算 290
13.10.1 Equational theory … 291 13.10.1 等式理論 291
13.10.2 A fixed-point operator … 292 13.10.2 不動点演算子 292
13.11 Further reading … 295 13.11 さらなる読書 295
14 Nondeterminism and parallelism 14 非決定性と並列性
14.1 Introduction … 297 14.1 導入 297
14.2 Guarded commands … 298 14.2 ガード付きコマンド 298
14.3 Communicating processes … 303 14.3 通信プロセス 303
14.4 Milner's CCS … 308 14.4 ミルナーのCCS 308
14.5 Pure CCS … 311 14.5 純粋CCS 311
14.6 A specification language … 316 14.6 仕様言語 316
14.7 The modal μ-calculus … 321 14.7 モーダルμ計算 321
14.8 Local model checking … 327 14.8 ローカルモデルチェック 327
14.9 Further reading … 335 14.9 さらなる読書 335
Appendix 付録
A Incompleteness and undecidability … 337 A 不完全性と非決定可能性 337
Bibliography … 353 参考文献 353
Index … 357 索引 357
翻訳本: 『プログラミング言語の形式的意味論入門』
メモ
決定表からの共起集合を用いた新しいルール帰納法【JST・京大機械翻訳】 | 文献情報 | J-GLOBAL 科学技術総合リンクセンター
『プログラミング言語の形式的意味論入門』サポートサイト
#文献